Nuprl Lemma : free-from-atom_wf2
11,40
postcript
pdf
T
:Type,
x
:
T
,
a
:Atom2.
x
:
T
||
a
latex
Definitions
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
member
wf
origin
T:Type, x:T, a:Atom2. x:T||a 
T:Type, x:T, a:Atom2. x:T||a Tx:A. B(x)